


`include "package.sv"
program assertions(DDR_bus IF);
                    
            
property RASL2RASH;  //verify RAS fall and rise time....should this change?
	$fell(IF.RAS) |-> ##tRCD $rose(IF.RAS);
endproperty

assert property (@(posedge IF.CK) RASL2RASH)
    else $info("RAS delay incorrect");


property CASL2CASH;  //verify CAS fall and rise time
	$fell(IF.CAS) |-> ##tCL $rose(IF.CAS);
endproperty

assert property(@(posedge IF.CK) CASL2CASH)
  else $info("CAS delay incorrect");
 
 
 property BURST;
   $changed(IF.DQ) |-> ##tBURST $isunknown(IF.DQ);
 endproperty
   
/*   
property RASCASDQ;
     RASL2RASH |-> CASL2CASH |-> BURST;
endproperty

assert property (@(posedge IF.CK) RASCASDQ)
  else $info("RAS to CAS to DQ error");
    

property ACT2RD; //verify tRAS time between ACT and following PRE
	(IF.DDR_controller.State == IF.DDR_controller.ACTIVATE && IF.DDR_controller.OP == 0) 
	         |-> ##tRAS (IF.DDR_controller.State == IF.DDR_controller.READ);
endproperty

assert property(@(posedge IF.CK) ACT2RD)
  else $info ("ACTIVATE to READ incorrect delay");


property ACT2WR; //verify tRAS time between ACT and following PRE
	(IF.DDR_controller.State == IF.DDR_controller.ACTIVATE && IF.DDR_controller.OP == 1) 
	         |-> ##tRAS (IF.DDR_controller.State == IF.DDR_controller.WRITE);
endproperty

assert property(@(posedge IF.CK) ACT2WR)
  else $info ("ACTIVATE to WRITE incorrect delay");
*/

property RAS2CAS;  //Verify that CAS falls tRCD after RAS.
	$fell(IF.RAS) |-> ##tRCD $fell(IF.CAS);
endproperty

assert property (@(posedge IF.CK) RAS2CAS)
  else $info("RAS to CAS delay incorrect");


property BURST_ONLY;
	$changed(IF.DQ) |-> ##tBURST $isunknown(IF.DQ);
endproperty

assert property (@(posedge IF.CK) BURST_ONLY)
  else $info("Burst length incorrect");
    
/*
property ACT2IDLE;
    IF.DDR_controller.State == IF.DDR_controller.ACTIVATE |-> ##tRC IF.DDR_controller.State == IF.DDR_controller.IDLE;
endproperty
    
assert property(@(posedge IF.CK) ACT2IDLE)
  else $info("tRC delay after activate incorrect");
*/

property WE_AND_DQ;
  ($rose(IF.CAS) && $fell(IF.WE) && $changed(IF.DQ)) |-> ##tBURST ($rose(IF.WE) && $isunknown(IF.DQ));
endproperty

assert property (@(posedge IF.CK) WE_AND_DQ)
  else $info("Write Enable and DQ hold time incorrect");

/*

property TESTACT;  //test activate property..
//After a row is opened with an ACTIVATE command, a READ or WRITE command may be issued to that row, subject to the tRCD specification. 
//other tests should pick up where this leaves off
	@(posedge IF.CK)
	(IF.ENUM == ACT) |-> ($changed(IF.ADDRESS_LINE) ##[0:tRCD] ((IF.ENUM == RD || IF.ENUM == WR)));
endproperty


property TESTPRE;  //verify precharge time before activate is asserted
	@(posedge IF.CK)
	(IF.ENUM == PRE) ##tRP (IF.ENUM == ACT);
endproperty            
 
 
 
property ADDR2CAS;  //after row and ras, need column and CAS. can overlap
	@(posedge IF.CK)
	(ADDR2RAS |-> ($changed(IF.ADDRESS_LINE) ##tRCD $fell(IF.CAS));
endproperty
 
 */
  
  
  
endprogram
  
